$\forall$$A$:Type, $P$:($A$$\rightarrow$Prop), $B$:($A$$\rightarrow$Type). $a$:\{$a$:$A$$\mid$ $P$($a$) \} fp$\rightarrow$ $B$($a$) $\subseteq\rho$ $a$:$A$ fp$\rightarrow$ $B$($a$)